(set-logic QF_LRA)
(set-info :source | TTA Startup. Bruno Dutertre (bruno@csl.sri.com) |)
(set-info :smt-lib-version 2.0)
(set-info :category "industrial")
(set-info :status unsat)
(declare-fun x_0 () Real)
(declare-fun x_1 () Real)
(declare-fun x_2 () Real)
(declare-fun x_3 () Real)
(declare-fun x_4 () Real)
(declare-fun x_5 () Real)
(declare-fun x_6 () Real)
(declare-fun x_7 () Real)
(declare-fun x_8 () Real)
(declare-fun x_9 () Real)
(declare-fun x_10 () Real)
(declare-fun x_11 () Real)
(declare-fun x_12 () Real)
(declare-fun x_13 () Bool)
(declare-fun x_14 () Bool)
(declare-fun x_15 () Bool)
(declare-fun x_16 () Real)
(declare-fun x_17 () Real)
(declare-fun x_18 () Real)
(declare-fun x_19 () Real)
(declare-fun x_20 () Real)
(declare-fun x_21 () Real)
(declare-fun x_22 () Bool)
(declare-fun x_23 () Real)
(declare-fun x_24 () Bool)
(declare-fun x_25 () Bool)
(declare-fun x_26 () Bool)
(declare-fun x_27 () Real)
(declare-fun x_28 () Real)
(declare-fun x_29 () Real)
(declare-fun x_30 () Real)
(declare-fun x_31 () Real)
(declare-fun x_32 () Real)
(declare-fun x_33 () Real)
(declare-fun x_34 () Real)
(declare-fun x_35 () Real)
(declare-fun x_36 () Real)
(declare-fun x_37 () Real)
(declare-fun x_38 () Real)
(declare-fun x_39 () Real)
(declare-fun x_40 () Real)
(declare-fun x_41 () Real)
(declare-fun x_42 () Real)
(declare-fun x_43 () Real)
(declare-fun x_44 () Real)
(declare-fun x_45 () Real)
(declare-fun x_46 () Real)
(declare-fun x_47 () Real)
(declare-fun x_48 () Real)
(declare-fun x_49 () Bool)
(declare-fun x_50 () Real)
(declare-fun x_51 () Bool)
(declare-fun x_52 () Bool)
(declare-fun x_53 () Bool)
(declare-fun x_54 () Real)
(declare-fun x_55 () Real)
(declare-fun x_56 () Real)
(declare-fun x_57 () Real)
(declare-fun x_58 () Real)
(declare-fun x_59 () Real)
(declare-fun x_60 () Real)
(declare-fun x_61 () Real)
(declare-fun x_62 () Real)
(declare-fun x_63 () Real)
(assert (let ((?v_83 (= x_0 0)) (?v_95 (= x_0 1)) (?v_100 (= x_0 2)) (?v_127 (= x_3 0)) (?v_133 (= x_3 1)) (?v_137 (= x_3 2)) (?v_150 (= x_7 0)) (?v_156 (= x_7 1)) (?v_159 (= x_7 2)) (?v_170 (= x_10 0)) (?v_176 (= x_10 1)) (?v_179 (= x_10 2)) (?v_164 (= x_7 3)) (?v_152 (= x_1 x_8)) (?v_184 (= x_10 3)) (?v_172 (= x_1 x_11)) (?v_99 (= x_19 0)) (?v_69 (< x_1 x_2)) (?v_70 (< x_1 x_4)) (?v_71 (< x_1 x_8)) (?v_72 (< x_1 x_11)) (?v_105 (= x_0 3)) (?v_92 (= x_1 x_2)) (?v_142 (= x_3 3)) (?v_129 (= x_1 x_4)) (?v_9 (= x_21 4)) (?v_10 (= x_21 3)) (?v_11 (= x_21 2)) (?v_227 (not (< x_33 (+ x_34 24)))) (?v_229 (not (< x_35 (+ x_34 27)))) (?v_231 (not (< x_36 (+ x_34 30)))) (?v_233 (not (< x_37 (+ x_34 33)))) (?v_80 (= x_38 1)) (?v_93 (= x_38 2)) (?v_126 (= x_39 1)) (?v_130 (= x_39 2)) (?v_149 (= x_40 1)) (?v_153 (= x_40 2)) (?v_169 (= x_41 1)) (?v_173 (= x_41 2))) (let ((?v_199 (not ?v_80)) (?v_195 (not ?v_93)) (?v_200 (not ?v_126)) (?v_196 (not ?v_130)) (?v_201 (not ?v_149)) (?v_197 (not ?v_153)) (?v_202 (not ?v_169)) (?v_198 (not ?v_173)) (?v_26 (= x_40 3))) (let ((?v_34 (not ?v_26)) (?v_36 (not (= x_32 x_36))) (?v_27 (= x_41 3))) (let ((?v_37 (not ?v_27)) (?v_39 (not (= x_32 x_37))) (?v_213 (not (<= (- x_35 x_33) x_18))) (?v_214 (not (<= (- x_36 x_33) x_18))) (?v_215 (not (<= (- x_37 x_33) x_18))) (?v_216 (not (<= (- x_36 x_35) x_18))) (?v_217 (not (<= (- x_37 x_35) x_18))) (?v_218 (not (<= (- x_37 x_36) x_18))) (?v_222 (not (< (- x_33 x_34) 12))) (?v_209 (<= (- x_33 x_32) 12)) (?v_223 (not (< (- x_35 x_34) 15))) (?v_210 (<= (- x_35 x_32) 15)) (?v_224 (not (< (- x_36 x_34) 18))) (?v_211 (<= (- x_36 x_32) 18)) (?v_225 (not (< (- x_37 x_34) 21))) (?v_212 (<= (- x_37 x_32) 21)) (?v_32 (= x_43 x_44)) (?v_35 (= x_43 x_45)) (?v_38 (= x_43 x_46)) (?v_41 (= x_44 x_43)) (?v_45 (= x_44 x_45)) (?v_48 (= x_44 x_46)) (?v_50 (= x_45 x_43)) (?v_51 (= x_45 x_44)) (?v_52 (= x_45 x_46)) (?v_53 (= x_46 x_43)) (?v_54 (= x_46 x_44)) (?v_55 (= x_46 x_45)) (?v_261 (< x_32 x_33))) (let ((?v_30 (not ?v_261)) (?v_242 (= x_43 x_48)) (?v_262 (< x_32 x_35))) (let ((?v_40 (not ?v_262)) (?v_244 (= x_44 x_48)) (?v_264 (< x_32 x_36))) (let ((?v_44 (not ?v_264)) (?v_246 (= x_45 x_48)) (?v_266 (< x_32 x_37))) (let ((?v_47 (not ?v_266)) (?v_248 (= x_46 x_48)) (?v_23 (= x_38 3))) (let ((?v_28 (not ?v_23)) (?v_31 (not (= x_32 x_33))) (?v_24 (= x_39 3))) (let ((?v_29 (not ?v_24)) (?v_33 (not (= x_32 x_35))) (?v_226 (and x_49 (< x_50 x_33))) (?v_228 (and x_51 (< x_50 x_35))) (?v_230 (and x_52 (< x_50 x_36))) (?v_232 (and x_53 (< x_50 x_37))) (?v_16 (= x_48 4)) (?v_17 (= x_48 3)) (?v_18 (= x_48 2))) (let ((?v_240 (ite ?v_16 x_37 (ite ?v_17 x_36 (ite ?v_18 x_35 x_33)))) (?v_110 (not x_49)) (?v_147 (not x_51)) (?v_167 (not x_52)) (?v_187 (not x_53)) (?v_56 (< x_43 1)) (?v_239 (or (or (or x_49 x_51) x_52) x_53)) (?v_263 (= x_33 x_35)) (?v_265 (= x_33 x_36)) (?v_267 (= x_33 x_37)) (?v_270 (= x_35 x_33)) (?v_272 (= x_35 x_36)) (?v_274 (= x_35 x_37)) (?v_275 (= x_36 x_33)) (?v_276 (= x_36 x_35)) (?v_277 (= x_36 x_37)) (?v_278 (= x_37 x_33)) (?v_279 (= x_37 x_35)) (?v_280 (= x_37 x_36)) (?v_19 (= x_43 4))) (let ((?v_249 (ite ?v_19 1 (+ x_43 1))) (?v_20 (= x_44 4))) (let ((?v_250 (ite ?v_20 1 (+ x_44 1))) (?v_21 (= x_45 4))) (let ((?v_251 (ite ?v_21 1 (+ x_45 1))) (?v_22 (= x_46 4))) (let ((?v_252 (ite ?v_22 1 (+ x_46 1))) (?v_116 (= x_19 1)) (?v_12 (= x_5 4))) (let ((?v_65 (ite ?v_12 1 (+ x_5 1))) (?v_13 (= x_6 4))) (let ((?v_66 (ite ?v_13 1 (+ x_6 1))) (?v_14 (= x_9 4))) (let ((?v_67 (ite ?v_14 1 (+ x_9 1))) (?v_15 (= x_12 4))) (let ((?v_68 (ite ?v_15 1 (+ x_12 1))) (?v_84 (and (= x_42 x_19) (= x_50 x_23)))) (let ((?v_128 (and ?v_84 (= x_49 x_22))) (?v_85 (= x_51 x_24))) (let ((?v_151 (and ?v_128 ?v_85)) (?v_86 (= x_52 x_25))) (let ((?v_171 (and ?v_151 ?v_86)) (?v_87 (= x_53 x_26)) (?v_88 (= x_48 x_21)) (?v_89 (= x_34 x_17))) (let ((?v_81 (and (and (and ?v_171 ?v_87) ?v_88) ?v_89)) (?v_141 (= x_44 x_21)) (?v_163 (= x_45 x_21)) (?v_76 (= x_32 x_2)) (?v_77 (= x_32 x_4)) (?v_78 (= x_32 x_8)) (?v_79 (= x_32 x_11)) (?v_183 (= x_46 x_21)) (?v_96 (= x_1 x_23)) (?v_123 (= x_41 x_10)) (?v_124 (= x_46 x_12)) (?v_125 (= x_37 x_11)) (?v_90 (= x_38 x_0)) (?v_82 (= x_43 x_5)) (?v_91 (= x_33 x_2)) (?v_117 (= x_39 x_3)) (?v_118 (= x_44 x_6)) (?v_119 (= x_35 x_4)) (?v_120 (= x_40 x_7)) (?v_121 (= x_45 x_9)) (?v_122 (= x_36 x_8)) (?v_104 (= x_43 x_21)) (?v_74 (and (and (and (not x_22) (not x_24)) (not x_25)) (not x_26))) (?v_94 (= x_49 false))) (let ((?v_98 (and (and (and (and (and (and ?v_84 ?v_94) ?v_85) ?v_86) ?v_87) ?v_88) ?v_89)) (?v_132 (= x_51 false))) (let ((?v_135 (and (and (and (and (and ?v_128 ?v_132) ?v_86) ?v_87) ?v_88) ?v_89)) (?v_155 (= x_52 false))) (let ((?v_158 (and (and (and (and ?v_151 ?v_155) ?v_87) ?v_88) ?v_89)) (?v_175 (= x_53 false))) (let ((?v_178 (and (and (and ?v_171 ?v_175) ?v_88) ?v_89)) (?v_1 (or (not ?v_105) (not ?v_69))) (?v_0 (or (not ?v_142) (not ?v_70))) (?v_2 (or (not ?v_164) (not ?v_71))) (?v_3 (or (not ?v_184) (not ?v_72))) (?v_6 (not x_13)) (?v_4 (not x_14))) (let ((?v_7 (and ?v_6 ?v_4)) (?v_5 (not x_15))) (let ((?v_189 (and ?v_7 ?v_5)) (?v_8 (and x_13 ?v_4))) (let ((?v_203 (and ?v_8 ?v_5)) (?v_219 (and (and ?v_6 x_14) ?v_5)) (?v_235 (and (and x_13 x_14) ?v_5)) (?v_237 (and ?v_7 x_15)) (?v_257 (and ?v_8 x_15)) (?v_259 (or x_13 x_14)) (?v_260 (or ?v_6 x_14)) (?v_269 (and ?v_23 ?v_261)) (?v_268 (and ?v_24 ?v_262)) (?v_271 (and ?v_26 ?v_264)) (?v_273 (and ?v_27 ?v_266)) (?v_190 (and (and (and ?v_110 ?v_147) ?v_167) ?v_187)) (?v_241 (or ?v_28 ?v_30)) (?v_243 (or ?v_29 ?v_40)) (?v_245 (or ?v_34 ?v_44)) (?v_247 (or ?v_37 ?v_47)) (?v_58 (and ?v_199 ?v_195)) (?v_59 (and ?v_200 ?v_196)) (?v_61 (and ?v_201 ?v_197)) (?v_62 (and ?v_202 ?v_198)) (?v_25 (+ x_32 3)) (?v_42 (+ x_33 3)) (?v_43 (+ x_35 3)) (?v_46 (+ x_36 3)) (?v_49 (+ x_37 3)) (?v_57 (+ (+ x_33 (* (ite ?v_56 (- (- 1 x_43) 1) (- (+ (- 4 x_43) 1) 1)) 3)) x_18)) (?v_60 (+ (+ x_35 (* (ite (< x_44 2) (- (- 2 x_44) 1) (- (+ (- 4 x_44) 2) 1)) 3)) x_18)) (?v_63 (+ (+ x_36 (* (ite (< x_45 3) (- (- 3 x_45) 1) (- (+ (- 4 x_45) 3) 1)) 3)) x_18)) (?v_64 (+ (+ x_37 (* (ite (< x_46 4) (- x_47 1) (- (+ x_47 4) 1)) 3)) x_18))) (let ((?v_238 (and (and (and (and (and (and (and (and (and (and (and (and (and ?v_190 (or (or (or ?v_23 ?v_24) ?v_26) ?v_27)) (or ?v_28 (<= x_33 ?v_25))) (or ?v_29 (<= x_35 ?v_25))) (or ?v_34 (<= x_36 ?v_25))) (or ?v_37 (<= x_37 ?v_25))) (or ?v_28 (and (and (and (or (or ?v_241 ?v_31) (and (= x_43 x_55) (= x_33 ?v_42))) (or ?v_29 (and (and (or (or ?v_30 ?v_40) (and ?v_32 ?v_263)) (or (or ?v_31 ?v_33) ?v_32)) (or (or ?v_30 ?v_33) (and (= x_43 x_56) (= x_33 ?v_43)))))) (or ?v_34 (and (and (or (or ?v_30 ?v_44) (and ?v_35 ?v_265)) (or (or ?v_31 ?v_36) ?v_35)) (or (or ?v_30 ?v_36) (and (= x_43 x_57) (= x_33 ?v_46)))))) (or ?v_37 (and (and (or (or ?v_30 ?v_47) (and ?v_38 ?v_267)) (or (or ?v_31 ?v_39) ?v_38)) (or (or ?v_30 ?v_39) (and (= x_43 x_58) (= x_33 ?v_49)))))))) (or ?v_29 (and (and (and (or ?v_28 (and (and (or (or ?v_40 ?v_30) (and ?v_41 ?v_270)) (or (or ?v_33 ?v_31) ?v_41)) (or (or ?v_40 ?v_31) (and (= x_44 x_55) (= x_35 ?v_42))))) (or (or ?v_243 ?v_33) (and (= x_44 x_56) (= x_35 ?v_43)))) (or ?v_34 (and (and (or (or ?v_40 ?v_44) (and ?v_45 ?v_272)) (or (or ?v_33 ?v_36) ?v_45)) (or (or ?v_40 ?v_36) (and (= x_44 x_57) (= x_35 ?v_46)))))) (or ?v_37 (and (and (or (or ?v_40 ?v_47) (and ?v_48 ?v_274)) (or (or ?v_33 ?v_39) ?v_48)) (or (or ?v_40 ?v_39) (and (= x_44 x_58) (= x_35 ?v_49)))))))) (or ?v_34 (and (and (and (or ?v_28 (and (and (or (or ?v_44 ?v_30) (and ?v_50 ?v_275)) (or (or ?v_36 ?v_31) ?v_50)) (or (or ?v_44 ?v_31) (and (= x_45 x_55) (= x_36 ?v_42))))) (or ?v_29 (and (and (or (or ?v_44 ?v_40) (and ?v_51 ?v_276)) (or (or ?v_36 ?v_33) ?v_51)) (or (or ?v_44 ?v_33) (and (= x_45 x_56) (= x_36 ?v_43)))))) (or (or ?v_245 ?v_36) (and (= x_45 x_57) (= x_36 ?v_46)))) (or ?v_37 (and (and (or (or ?v_44 ?v_47) (and ?v_52 ?v_277)) (or (or ?v_36 ?v_39) ?v_52)) (or (or ?v_44 ?v_39) (and (= x_45 x_58) (= x_36 ?v_49)))))))) (or ?v_37 (and (and (and (or ?v_28 (and (and (or (or ?v_47 ?v_30) (and ?v_53 ?v_278)) (or (or ?v_39 ?v_31) ?v_53)) (or (or ?v_47 ?v_31) (and (= x_46 x_55) (= x_37 ?v_42))))) (or ?v_29 (and (and (or (or ?v_47 ?v_40) (and ?v_54 ?v_279)) (or (or ?v_39 ?v_33) ?v_54)) (or (or ?v_47 ?v_33) (and (= x_46 x_56) (= x_37 ?v_43)))))) (or ?v_34 (and (and (or (or ?v_47 ?v_44) (and ?v_55 ?v_280)) (or (or ?v_39 ?v_36) ?v_55)) (or (or ?v_47 ?v_36) (and (= x_46 x_57) (= x_37 ?v_46)))))) (or (or ?v_247 ?v_39) (and (= x_46 x_58) (= x_37 ?v_49)))))) (or ?v_28 (and (and (and (or ?v_58 (not (<= x_33 ?v_57))) (or ?v_59 (not (<= x_35 ?v_57)))) (or ?v_61 (not (<= x_36 ?v_57)))) (or ?v_62 (not (<= x_37 ?v_57)))))) (or ?v_29 (and (and (and (or ?v_58 (not (<= x_33 ?v_60))) (or ?v_59 (not (<= x_35 ?v_60)))) (or ?v_61 (not (<= x_36 ?v_60)))) (or ?v_62 (not (<= x_37 ?v_60)))))) (or ?v_34 (and (and (and (or ?v_58 (not (<= x_33 ?v_63))) (or ?v_59 (not (<= x_35 ?v_63)))) (or ?v_61 (not (<= x_36 ?v_63)))) (or ?v_62 (not (<= x_37 ?v_63)))))) (or ?v_37 (and (and (and (or ?v_58 (not (<= x_33 ?v_64))) (or ?v_59 (not (<= x_35 ?v_64)))) (or ?v_61 (not (<= x_36 ?v_64)))) (or ?v_62 (not (<= x_37 ?v_64))))))) (?v_73 (and (and (and ?v_69 ?v_70) ?v_71) ?v_72)) (?v_75 (and (and (and (<= x_32 x_2) (<= x_32 x_4)) (<= x_32 x_8)) (<= x_32 x_11))) (?v_97 (+ x_1 12))) (let ((?v_101 (= x_33 ?v_97)) (?v_109 (= x_50 (ite ?v_74 (+ x_1 x_18) x_23)))) (let ((?v_131 (and (= x_42 (ite ?v_74 0 x_19)) ?v_109)) (?v_111 (= x_51 (or ?v_74 x_24))) (?v_112 (= x_52 (or ?v_74 x_25))) (?v_113 (= x_53 (or ?v_74 x_26))) (?v_114 (= x_48 (ite ?v_74 1 x_21))) (?v_115 (= x_34 (ite ?v_74 x_1 x_17)))) (let ((?v_102 (and (and (and (and (and (and ?v_131 ?v_94) ?v_111) ?v_112) ?v_113) ?v_114) ?v_115)) (?v_106 (+ x_1 3))) (let ((?v_136 (- ?v_106 x_18))) (let ((?v_103 (= x_33 ?v_136)) (?v_107 (and ?v_105 ?v_92)) (?v_108 (= x_33 ?v_106)) (?v_145 (= x_42 (ite ?v_74 1 x_19))) (?v_134 (+ x_1 15))) (let ((?v_138 (= x_35 ?v_134)) (?v_146 (= x_49 (or ?v_74 x_22)))) (let ((?v_154 (and ?v_131 ?v_146)) (?v_148 (= x_48 (ite ?v_74 2 x_21)))) (let ((?v_139 (and (and (and (and (and ?v_154 ?v_132) ?v_112) ?v_113) ?v_148) ?v_115)) (?v_140 (= x_35 ?v_136)) (?v_143 (and ?v_142 ?v_129)) (?v_144 (= x_35 ?v_106)) (?v_157 (+ x_1 18))) (let ((?v_160 (= x_36 ?v_157)) (?v_174 (and ?v_154 ?v_111)) (?v_168 (= x_48 (ite ?v_74 3 x_21)))) (let ((?v_161 (and (and (and (and ?v_174 ?v_155) ?v_113) ?v_168) ?v_115)) (?v_162 (= x_36 ?v_136)) (?v_165 (and ?v_164 ?v_152)) (?v_166 (= x_36 ?v_106)) (?v_177 (+ x_1 21))) (let ((?v_180 (= x_37 ?v_177)) (?v_188 (= x_48 (ite ?v_74 4 x_21)))) (let ((?v_181 (and (and (and (and ?v_174 ?v_112) ?v_175) ?v_188) ?v_115)) (?v_182 (= x_37 ?v_136)) (?v_185 (and ?v_184 ?v_172)) (?v_186 (= x_37 ?v_106)) (?v_191 (or (= x_38 0) ?v_80)) (?v_192 (or (= x_39 0) ?v_126)) (?v_193 (or (= x_40 0) ?v_149)) (?v_194 (or (= x_41 0) ?v_169)) (?v_221 (and (and ?v_239 (= x_42 0)) (= x_54 2)))) (let ((?v_205 (or ?v_191 ?v_93)) (?v_206 (or ?v_192 ?v_130)) (?v_207 (or ?v_193 ?v_153)) (?v_208 (or ?v_194 ?v_173))) (let ((?v_204 (and (and (and (and (and (and (and (and (and (and (and (and ?v_221 ?v_205) ?v_206) ?v_207) ?v_208) (or ?v_195 (and (and ?v_110 ?v_222) ?v_209))) (or ?v_196 (and (and ?v_147 ?v_223) ?v_210))) (or ?v_197 (and (and ?v_167 ?v_224) ?v_211))) (or ?v_198 (and (and ?v_187 ?v_225) ?v_212))) (or (or ?v_199 x_49) ?v_227)) (or (or ?v_200 x_51) ?v_229)) (or (or ?v_201 x_52) ?v_231)) (or (or ?v_202 x_53) ?v_233))) (?v_220 (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and ?v_190 (or (or (or ?v_93 ?v_130) ?v_153) ?v_173)) ?v_205) ?v_206) ?v_207) ?v_208) (or ?v_195 ?v_209)) (or ?v_196 ?v_210)) (or ?v_197 ?v_211)) (or ?v_198 ?v_212)) (or ?v_195 (and (and (or ?v_196 ?v_213) (or ?v_197 ?v_214)) (or ?v_198 ?v_215)))) (or ?v_196 (and (or ?v_197 ?v_216) (or ?v_198 ?v_217)))) (or (or ?v_197 ?v_198) ?v_218)) (or ?v_195 (and (and (and (or ?v_199 (not (<= (- x_33 x_33) x_18))) (or ?v_200 ?v_213)) (or ?v_201 ?v_214)) (or ?v_202 ?v_215)))) (or ?v_196 (and (and (and (or ?v_199 (not (<= (- x_33 x_35) x_18))) (or ?v_200 (not (<= (- x_35 x_35) x_18)))) (or ?v_201 ?v_216)) (or ?v_202 ?v_217)))) (or ?v_197 (and (and (and (or ?v_199 (not (<= (- x_33 x_36) x_18))) (or ?v_200 (not (<= (- x_35 x_36) x_18)))) (or ?v_201 (not (<= (- x_36 x_36) x_18)))) (or ?v_202 ?v_218)))) (or ?v_198 (and (and (and (or ?v_199 (not (<= (- x_33 x_37) x_18))) (or ?v_200 (not (<= (- x_35 x_37) x_18)))) (or ?v_201 (not (<= (- x_36 x_37) x_18)))) (or ?v_202 (not (<= (- x_37 x_37) x_18))))))) (?v_253 (or (or ?v_199 ?v_226) ?v_227)) (?v_254 (or (or ?v_200 ?v_228) ?v_229)) (?v_255 (or (or ?v_201 ?v_230) ?v_231)) (?v_256 (or (or ?v_202 ?v_232) ?v_233)) (?v_234 (+ x_34 3))) (let ((?v_236 (and (and (and (and (and (and (and (and (and (and (and (and (and (and ?v_221 (= ?v_240 (+ (+ x_34 (* (- x_48 1) 3)) 12))) (not (ite ?v_16 x_53 (ite ?v_17 x_52 (ite ?v_18 x_51 x_49))))) (or (or (or ?v_195 (= 1 x_48)) ?v_226) (and ?v_222 ?v_209))) (or (or (or ?v_196 (= 2 x_48)) ?v_228) (and ?v_223 ?v_210))) (or (or (or ?v_197 (= 3 x_48)) ?v_230) (and ?v_224 ?v_211))) (or (or (or ?v_198 (= 4 x_48)) ?v_232) (and ?v_225 ?v_212))) ?v_253) ?v_254) ?v_255) ?v_256) (or ?v_28 (and ?v_242 (= x_33 ?v_234)))) (or ?v_29 (and ?v_244 (= x_35 ?v_234)))) (or ?v_34 (and ?v_246 (= x_36 ?v_234)))) (or ?v_37 (and ?v_248 (= x_37 ?v_234))))) (?v_258 (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and ?v_239 (= x_42 1)) (= x_54 3)) (= (ite ?v_16 x_46 (ite ?v_17 x_45 (ite ?v_18 x_44 x_43))) x_48)) (= ?v_240 ?v_234)) (or ?v_241 (and ?v_242 (= x_33 ?v_240)))) (or ?v_243 (and ?v_244 (= x_35 ?v_240)))) (or ?v_245 (and ?v_246 (= x_36 ?v_240)))) (or ?v_247 (and ?v_248 (= x_37 ?v_240)))) (or (or ?v_28 ?v_31) (and (= ?v_249 x_48) (= ?v_240 ?v_42)))) (or (or ?v_29 ?v_33) (and (= ?v_250 x_48) (= ?v_240 ?v_43)))) (or (or ?v_34 ?v_36) (and (= ?v_251 x_48) (= ?v_240 ?v_46)))) (or (or ?v_37 ?v_39) (and (= ?v_252 x_48) (= ?v_240 ?v_49)))) ?v_253) ?v_254) ?v_255) ?v_256) (or ?v_195 ?v_226)) (or ?v_196 ?v_228)) (or ?v_197 ?v_230)) (or ?v_198 ?v_232)))) (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (<= x_59 6) (>= x_59 0)) (<= x_54 3)) (>= x_54 0)) (<= x_42 1)) (>= x_42 0)) (<= x_41 3)) (>= x_41 0)) (<= x_40 3)) (>= x_40 0)) (<= x_39 3)) (>= x_39 0)) (<= x_38 3)) (>= x_38 0)) (<= x_27 3)) (>= x_27 0)) (<= x_19 1)) (>= x_19 0)) (<= x_16 6)) (>= x_16 0)) (<= x_10 3)) (>= x_10 0)) (<= x_7 3)) (>= x_7 0)) (<= x_3 3)) (>= x_3 0)) (<= x_0 3)) (>= x_0 0)) (or (or (or (= x_5 1) (= x_5 2)) (= x_5 3)) ?v_12)) (not (< x_5 1))) (<= x_5 4)) (or (or (or (= x_6 1) (= x_6 2)) (= x_6 3)) ?v_13)) (not (< x_6 1))) (<= x_6 4)) (or (or (or (= x_9 1) (= x_9 2)) (= x_9 3)) ?v_14)) (not (< x_9 1))) (<= x_9 4)) (or (or (or (= x_12 1) (= x_12 2)) (= x_12 3)) ?v_15)) (not (< x_12 1))) (<= x_12 4)) (> x_18 0)) (< x_18 (/ 3 2))) (or (or (or (= x_21 1) ?v_11) ?v_10) ?v_9)) (not (< x_21 1))) (<= x_21 4)) (or (or (or (= x_43 1) (= x_43 2)) (= x_43 3)) ?v_19)) (not ?v_56)) (<= x_43 4)) (or (or (or (= x_44 1) (= x_44 2)) (= x_44 3)) ?v_20)) (not (< x_44 1))) (<= x_44 4)) (or (or (or (= x_45 1) (= x_45 2)) (= x_45 3)) ?v_21)) (not (< x_45 1))) (<= x_45 4)) (or (or (or (= x_46 1) (= x_46 2)) (= x_46 3)) ?v_22)) (not (< x_46 1))) (<= x_46 4)) (or (or (or (= x_48 1) ?v_18) ?v_17) ?v_16)) (not (< x_48 1))) (<= x_48 4)) (or ?v_1 (and (and (or ?v_0 (and (= x_2 x_4) (= x_5 x_6))) (or ?v_2 (and (= x_2 x_8) (= x_5 x_9)))) (or ?v_3 (and (= x_2 x_11) (= x_5 x_12)))))) (or ?v_0 (and (and (or ?v_1 (and (= x_4 x_2) (= x_6 x_5))) (or ?v_2 (and (= x_4 x_8) (= x_6 x_9)))) (or ?v_3 (and (= x_4 x_11) (= x_6 x_12)))))) (or ?v_2 (and (and (or ?v_1 (and (= x_8 x_2) (= x_9 x_5))) (or ?v_0 (and (= x_8 x_4) (= x_9 x_6)))) (or ?v_3 (and (= x_8 x_11) (= x_9 x_12)))))) (or ?v_3 (and (and (or ?v_1 (and (= x_11 x_2) (= x_12 x_5))) (or ?v_0 (and (= x_11 x_4) (= x_12 x_6)))) (or ?v_2 (and (= x_11 x_8) (= x_12 x_9)))))) (or (or (or (or (or (= x_16 0) (= x_16 1)) (= x_16 2)) (= x_16 3)) (= x_16 4)) (= x_16 5))) (or (or (or (or (or ?v_189 ?v_203) ?v_219) ?v_235) ?v_237) ?v_257)) (= x_20 (- 4 x_12))) (= x_27 (ite ?v_9 x_10 (ite ?v_10 x_7 (ite ?v_11 x_3 x_0))))) (= x_28 ?v_65)) (= x_29 ?v_66)) (= x_30 ?v_67)) (= x_31 ?v_68)) (= x_47 (- 4 x_46))) (= x_54 (ite ?v_16 x_41 (ite ?v_17 x_40 (ite ?v_18 x_39 x_38))))) (= x_55 ?v_249)) (= x_56 ?v_250)) (= x_57 ?v_251)) (= x_58 ?v_252)) (= x_59 (ite ?v_238 4 6))) (= x_60 ?v_65)) (= x_61 ?v_66)) (= x_62 ?v_67)) (= x_63 ?v_68)) (or (and (and (and (and (and (and (and (and (and (and (and (and (and (and (ite ?v_74 ?v_73 (and ?v_73 (< x_1 x_23))) (ite ?v_74 (and ?v_75 (or (or (or ?v_76 ?v_77) ?v_78) ?v_79)) (and (and ?v_75 (<= x_32 x_23)) (or (or (or (or (= x_32 x_23) ?v_76) ?v_77) ?v_78) ?v_79)))) ?v_90) ?v_117) ?v_120) ?v_123) ?v_82) ?v_118) ?v_121) ?v_124) ?v_91) ?v_119) ?v_122) ?v_125) ?v_81) (and (or (or (or (and (and (and (and (and (and (and (and (and (or (or (or (or (or (or (or (or (or (and (and (and (and (and ?v_83 ?v_92) ?v_80) (= x_33 (+ x_1 24))) ?v_81) ?v_82) (and (and (and (and (and (and ?v_83 x_22) ?v_96) ?v_98) ?v_90) ?v_82) ?v_91)) (and (and (and (and (and ?v_95 ?v_92) ?v_93) ?v_101) ?v_102) ?v_82)) (and (and (and (and (and (and (and ?v_95 x_22) ?v_99) ?v_96) ?v_93) (= x_33 (- ?v_97 x_18))) ?v_98) ?v_82)) (and (and (and (and (and (and (and ?v_100 x_22) ?v_99) ?v_96) ?v_23) ?v_103) ?v_104) ?v_98)) (and (and (and (and (and ?v_100 ?v_92) ?v_101) ?v_102) ?v_90) ?v_82)) (and (and (and (and (and (and (and (or ?v_95 ?v_100) x_22) ?v_116) ?v_96) ?v_23) ?v_103) ?v_104) ?v_98)) (and (and (and (and (and ?v_107 (not (= ?v_65 1))) ?v_108) (= x_43 x_60)) ?v_81) ?v_90)) (and (and (and (and (and (and (and (and (and (and (and (and ?v_107 (= x_60 1)) ?v_108) (= x_43 ?v_65)) ?v_145) ?v_109) ?v_110) ?v_111) ?v_112) ?v_113) ?v_114) ?v_115) ?v_90)) (and (and (and (and (and (and (and ?v_105 x_22) ?v_116) ?v_96) ?v_98) ?v_90) ?v_82) ?v_91)) ?v_117) ?v_118) ?v_119) ?v_120) ?v_121) ?v_122) ?v_123) ?v_124) ?v_125) (and (and (and (and (and (and (and (and (and (or (or (or (or (or (or (or (or (or (and (and (and (and (and ?v_127 ?v_129) ?v_126) (= x_35 (+ x_1 27))) ?v_81) ?v_118) (and (and (and (and (and (and ?v_127 x_24) ?v_96) ?v_135) ?v_117) ?v_118) ?v_119)) (and (and (and (and (and ?v_133 ?v_129) ?v_130) ?v_138) ?v_139) ?v_118)) (and (and (and (and (and (and (and ?v_133 x_24) ?v_99) ?v_96) ?v_130) (= x_35 (- ?v_134 x_18))) ?v_135) ?v_118)) (and (and (and (and (and (and (and ?v_137 x_24) ?v_99) ?v_96) ?v_24) ?v_140) ?v_141) ?v_135)) (and (and (and (and (and ?v_137 ?v_129) ?v_138) ?v_139) ?v_117) ?v_118)) (and (and (and (and (and (and (and (or ?v_133 ?v_137) x_24) ?v_116) ?v_96) ?v_24) ?v_140) ?v_141) ?v_135)) (and (and (and (and (and ?v_143 (not (= ?v_66 2))) ?v_144) (= x_44 x_61)) ?v_81) ?v_117)) (and (and (and (and (and (and (and (and (and (and (and (and ?v_143 (= x_61 2)) ?v_144) (= x_44 ?v_66)) ?v_145) ?v_109) ?v_146) ?v_147) ?v_112) ?v_113) ?v_148) ?v_115) ?v_117)) (and (and (and (and (and (and (and ?v_142 x_24) ?v_116) ?v_96) ?v_135) ?v_117) ?v_118) ?v_119)) ?v_90) ?v_82) ?v_91) ?v_120) ?v_121) ?v_122) ?v_123) ?v_124) ?v_125)) (and (and (and (and (and (and (and (and (and (or (or (or (or (or (or (or (or (or (and (and (and (and (and ?v_150 ?v_152) ?v_149) (= x_36 (+ x_1 30))) ?v_81) ?v_121) (and (and (and (and (and (and ?v_150 x_25) ?v_96) ?v_158) ?v_120) ?v_121) ?v_122)) (and (and (and (and (and ?v_156 ?v_152) ?v_153) ?v_160) ?v_161) ?v_121)) (and (and (and (and (and (and (and ?v_156 x_25) ?v_99) ?v_96) ?v_153) (= x_36 (- ?v_157 x_18))) ?v_158) ?v_121)) (and (and (and (and (and (and (and ?v_159 x_25) ?v_99) ?v_96) ?v_26) ?v_162) ?v_163) ?v_158)) (and (and (and (and (and ?v_159 ?v_152) ?v_160) ?v_161) ?v_120) ?v_121)) (and (and (and (and (and (and (and (or ?v_156 ?v_159) x_25) ?v_116) ?v_96) ?v_26) ?v_162) ?v_163) ?v_158)) (and (and (and (and (and ?v_165 (not (= ?v_67 3))) ?v_166) (= x_45 x_62)) ?v_81) ?v_120)) (and (and (and (and (and (and (and (and (and (and (and (and ?v_165 (= x_62 3)) ?v_166) (= x_45 ?v_67)) ?v_145) ?v_109) ?v_146) ?v_111) ?v_167) ?v_113) ?v_168) ?v_115) ?v_120)) (and (and (and (and (and (and (and ?v_164 x_25) ?v_116) ?v_96) ?v_158) ?v_120) ?v_121) ?v_122)) ?v_90) ?v_82) ?v_91) ?v_117) ?v_118) ?v_119) ?v_123) ?v_124) ?v_125)) (and (and (and (and (and (and (and (and (and (or (or (or (or (or (or (or (or (or (and (and (and (and (and ?v_170 ?v_172) ?v_169) (= x_37 (+ x_1 33))) ?v_81) ?v_124) (and (and (and (and (and (and ?v_170 x_26) ?v_96) ?v_178) ?v_123) ?v_124) ?v_125)) (and (and (and (and (and ?v_176 ?v_172) ?v_173) ?v_180) ?v_181) ?v_124)) (and (and (and (and (and (and (and ?v_176 x_26) ?v_99) ?v_96) ?v_173) (= x_37 (- ?v_177 x_18))) ?v_178) ?v_124)) (and (and (and (and (and (and (and ?v_179 x_26) ?v_99) ?v_96) ?v_27) ?v_182) ?v_183) ?v_178)) (and (and (and (and (and ?v_179 ?v_172) ?v_180) ?v_181) ?v_123) ?v_124)) (and (and (and (and (and (and (and (or ?v_176 ?v_179) x_26) ?v_116) ?v_96) ?v_27) ?v_182) ?v_183) ?v_178)) (and (and (and (and (and ?v_185 (not (= ?v_68 4))) ?v_186) (= x_46 x_63)) ?v_81) ?v_123)) (and (and (and (and (and (and (and (and (and (and (and (and ?v_185 (= x_63 4)) ?v_186) (= x_46 ?v_68)) ?v_145) ?v_109) ?v_146) ?v_111) ?v_112) ?v_187) ?v_188) ?v_115) ?v_123)) (and (and (and (and (and (and (and ?v_184 x_26) ?v_116) ?v_96) ?v_178) ?v_123) ?v_124) ?v_125)) ?v_90) ?v_82) ?v_91) ?v_117) ?v_118) ?v_119) ?v_120) ?v_121) ?v_122)) (= x_32 x_1)))) (or (or (or (or (or (or (and ?v_189 (= x_16 (ite (and (and (and (and ?v_190 ?v_191) ?v_192) ?v_193) ?v_194) 0 (ite ?v_204 1 6)))) (and ?v_203 (= x_16 (ite ?v_204 1 (ite ?v_220 2 6))))) (and ?v_219 (= x_16 (ite ?v_220 2 (ite ?v_236 3 6))))) (and ?v_235 (= x_16 (ite ?v_236 3 (ite ?v_220 2 x_59))))) (and ?v_237 (= x_16 (ite ?v_238 4 (ite ?v_258 5 6))))) (and ?v_257 (= x_16 (ite ?v_258 5 x_59)))) (and (and (and (and (and (and (or ?v_259 x_15) (or ?v_260 x_15)) (or (or x_13 ?v_4) x_15)) (or (or ?v_6 ?v_4) x_15)) (or ?v_259 ?v_5)) (or ?v_260 ?v_5)) (= x_16 6)))) (or (or (or (and ?v_269 (or (or (and ?v_268 (or (not ?v_263) (not ?v_32))) (and ?v_271 (or (not ?v_265) (not ?v_35)))) (and ?v_273 (or (not ?v_267) (not ?v_38))))) (and ?v_268 (or (or (and ?v_269 (or (not ?v_270) (not ?v_41))) (and ?v_271 (or (not ?v_272) (not ?v_45)))) (and ?v_273 (or (not ?v_274) (not ?v_48)))))) (and ?v_271 (or (or (and ?v_269 (or (not ?v_275) (not ?v_50))) (and ?v_268 (or (not ?v_276) (not ?v_51)))) (and ?v_273 (or (not ?v_277) (not ?v_52)))))) (and ?v_273 (or (or (and ?v_269 (or (not ?v_278) (not ?v_53))) (and ?v_268 (or (not ?v_279) (not ?v_54)))) (and ?v_271 (or (not ?v_280) (not ?v_55))))))) (or (or ?v_5 ?v_4) ?v_6)))))))))))))))))))))))))))))))))))))))))))))))))
(check-sat)
(exit)
